Nuprl Lemma : rem_bounds_3
13,42
postcript
pdf
a
:{...0},
n
:{...-1}. (0
(
a
rem
n
) ) & ((
a
rem
n
) >
n
)
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
False
,
P
Q
,
A
,
A
B
,
{...
i
}
Lemmas
int
lower
wf
origin
a:{...0}, n:{...-1}. (0 
(a rem n) ) & ((a rem n) > n) a:{...0}, n:{...-1}. (0 (a rem n) ) & ((a rem n) > n) 
Tx:A. B(x)
Q
A
B